We repeat the statement of Page \pageref{th:scccs}:
\begin{theorem}[Strong Compatibility]
Let $P,Q$ be \evold{2} processes such that $P \preceq Q$.
Then, $P \pired P'$ implies that there exists $Q'$ such that $Q \pired Q'$ and $P' \preceq Q'$. 
\end{theorem}
%\begin{proof}[Sketch]
\begin{proof}
\todo{This needs to be more formal, using contexts already defined.}
By case analysis on the rule used to infer reduction $P \pired P'$. 
We content ourselves with illustrating the case of update.
We then  assume
$$P = \mathtt{C_1}(\ \mathtt{C_2}(\component{a}{P_1}) \parallel \mathtt{C_3}(\update{a}{P_{2}}.R)\ ),$$ 
where
$\mathtt{C}( Q )$ denotes a term $\mathtt{C}$ with a hole 
which is filled with the term $Q$.   
%Other cases are similar or simpler.
Let $m$ be the node labeled $\update{a}{P_{2}}.R$, %appears, 
and $n$ the root labeled $a$ of the tree $\component{a}{P_1}$.

We first consider the modifications to $\Tree(P)$ when $P \pired P'$. The tree $\Tree(P')$ is obtained from $\Tree(P)$ in the following way:
\begin{enumerate}
\item the node labeled %in which 
$\update{a}{P_2}.R$ %occurs 
is replaced with $\Tree(R)$; 
%\item the label $a$ corresponding to component $\component{a}{P_1}$ is replaced with $t$; 
%
\item the tree rooted in $a[\ ]$ %subtree whose root is the child of the above node labeled %with label $t$ 
becomes $\Tree(\fillcon{P_2\,}{P_1})$ (thus replacing $\Tree(\component{a}{P_1})$).
\end{enumerate}

We know that since $P \preceq Q$, $\Tree(P) =^{\mathsf{tr}} \Tree(Q)$. 
Hence, there exists a mapping $f$ that associates nodes in $\Tree(P)$ to nodes in $\Tree(Q)$. 
This way there is a node $f(m)$ in $\Tree(Q)$ %that contains the 
labeled $\update{a}{P_2}.R$. Moreover, there exists another node $f(n)$ labeled with $a[\ ]$
which has a common ancestor with node $m$.
The update described above can therefore take place in $Q$ as well, and so $Q \pired Q'$.
Now, $\Tree(Q')$ is obtained from $\Tree(Q)$ by applying the same changes described above to the target nodes (of the adaptable process $a$ and of the
update  $\update{a}{P_2}.R$) according to $f$.

The last thing to show is that $P' \preceq Q'$, which follows 
 by observing that the mapping between $\Tree(P')$ and $\Tree(Q')$ is the same mapping $f$  
 between $\Tree(P)$ and $\Tree(Q)$, for all the nodes that have not been modified by the reduction and 
 that there is a correspondence one to one for the other nodes. More precisely: 
\begin{enumerate}
 \item Consider the labels in node $f(m)$: all nodes removed in $\Tree(P')$ have been removed in $\Tree(Q')$, hence the nodes $m$ and $f(m)$ are still in relation.
%  \item Let us now consider the tree radicated in $f(n)$: Nodes do not disappear as the label $a$ is replaced with $t$ both in $n$ and $f(n)$.
%  Hence, it is not possible that two different levels are merged and the two nodes are still in relation.
 \item Finally, we consider the two trees rooted in $n$ and $f(n)$: 
 $S= \Tree(\fillcon{P_2\,}{P_1})$ and 
 $T=\Tree(\fillcon{P_2\,}{Q_1})$, respectively. $S$ is the same subtree as $T$ apart from some subtrees of $P_1$ and $Q_1$ that can be put easily in relation %as $t$ is the same in both subtrees and 
as the subtrees $\Tree(P_1)$ and $\Tree(Q_1)$ are in relation with $f$.
% Similarly as before the reserved name $t$ guarantees that different levels (not in relation with $f$) are merged.
 \end{enumerate}
Thus $\Tree(P')=^{\mathsf{tr}} \Tree(Q')$. %\qed
\end{proof}
